theory Design_Sec_CloseSession imports "../Design_Instantiation" "../Specification/Design_CloseSession" begin section "auxiliary lemma" lemma Driver_Read_not_change_old: "∀s. (⇑(Driver_Read s smc_ex_init_read zx_mgr)) = ⇑s" using Driver_Read_def by simp lemma abs_rev_lemma:"(⇑(s⇓t)) =t" by auto lemma TA_CloseSessionEntryPointR_refine: "∀s. (TA_CloseSessionEntryPoint (⇑s) tid) = ⇑(TA_CloseSessionEntryPointR s tid)" proof - { fix s let ?s' = "(TA_CloseSessionEntryPointR s tid)" let ?t = "⇑s" let ?t' = "(TA_CloseSessionEntryPoint (⇑s) tid)" have a0: "current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t" by simp have a01: "?t' =⇑(?s')" using TA_CloseSessionEntryPointR_def by auto } then show ?thesis by blast qed lemma Driver_Write_smc_not_change_old: "∀s. (⇑(fst(Driver_Write_smc s zx_mgr ZX_OKr smc_ex_init))) = (⇑s)" using Driver_Write_smc_def by auto lemma TEEC_CloseSession1R_notchnew: assumes p1: "s'=(fst(TEEC_CloseSession1R sysconf s fd ses_id in_params out_params))" shows "(s ∼. d .∼Δ s')" using TEEC_CloseSession1R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma TEE_CloseTASession1R_notchnew: assumes p1: "s'=(fst(TEE_CloseTASession1R sysconf s))" shows "(s ∼. d .∼Δ s')" using TEE_CloseTASession1R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma TEE_CloseTASession2R_notchnew: assumes p1: "s'=(fst(TEE_CloseTASession2R sysconf s))" shows "(s ∼. d .∼Δ s')" using TEE_CloseTASession2R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma TEE_CloseTASession4R_notchnew: assumes p1: "s'=(fst(TEE_CloseTASession4R sysconf s))" shows "(s ∼. d .∼Δ s')" using TEE_CloseTASession4R_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) lemma isSesIdinMgrSesList_cur_ta_session_listR: "∀ s ses_id t ses_id_t. ses_id = ses_id_t ∧ ta_mgr (TEE_state s) = ta_mgr (TEE_state t) ⟶ isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the ses_id) = isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state t))) (the ses_id_t)" proof- { fix s::"StateR" fix t::"StateR" fix ses_id::"SESSION_ID_TYPE option" fix ses_id_t::"SESSION_ID_TYPE option" let ?isSesIdinMgrSesList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state s))) (the ses_id)" let ?isSesIdinMgrSesList_t = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state t))) (the ses_id_t)" assume a1: "ses_id = ses_id_t" assume a2: "ta_mgr (TEE_state s) = ta_mgr (TEE_state t)" have b1: "(mgr_ta_sessions (ta_mgr (TEE_state s))) = (mgr_ta_sessions (ta_mgr (TEE_state t)))" using a1 a2 by auto have b2: "?isSesIdinMgrSesList = ?isSesIdinMgrSesList_t" using b1 a1 by auto } then show ?thesis by auto qed lemma tee_ta_close_session_teeDomain2_preR_notchnew: assumes p1: "s'=(fst (tee_ta_close_session_teeDomain2_preR sc s tar_ses_id clientType params_in params_out))" shows "(s ∼. d .∼Δ s')" using tee_ta_close_session_teeDomain2_preR_def abstract_state_def abstract_state_rev_def vpeq_ipc_def by (smt (verit) Pair_inject State.ext_inject State.update_convs(1) State.update_convs(2) State.update_convs(3) State.update_convs(4) State.update_convs(5) State.update_convs(6) StateR.ext_inject StateR.surjective p1 surjective_pairing ) section "TEEC side" subsection "CloseSession_refine" lemma TEEC_CloseSession1R_refine: "∀s. fst (TEEC_CloseSession1 sc (⇑s) fd ses_id in_params out_params) = ⇑(fst (TEEC_CloseSession1R sc s fd ses_id in_params out_params))" proof - { fix ss :: StateR have "∀s sa. ⇑s⇓sa = sa" by simp then have "fst (TEEC_CloseSession1 sc ⇑ss fd ses_id in_params out_params) = ⇑fst (TEEC_CloseSession1R sc ss fd ses_id in_params out_params)" by (metis (no_types) TEEC_CloseSession1R_def fst_conv) } then show ?thesis by metis qed lemma TEEC_CloseSession2R_refine: "∀s. fst (TEEC_CloseSession2 sc (⇑s)) = ⇑(fst (TEEC_CloseSession2R sc s))" proof - { fix s let ?s' = "fst(TEEC_CloseSession2R sc s)" let ?t = "⇑s" let ?t' = "fst(TEEC_CloseSession2 sc ?t)" have a0: "current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t" by simp have a01: "?t' =⇑(?s')" proof - { show ?thesis proof (cases"(current s ≠ TEE sc)∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS2)") case True have a1: "(current s ≠ TEE sc)∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS2)" using True by blast have a2: "?t=?t'" using TEEC_CloseSession2_def a1 by (smt (verit, ccfv_threshold) a0 fstI) have a3: "s=?s'" using TEEC_CloseSession2R_def a1 by (smt (verit, best) fstI) show ?thesis using a2 a3 by simp next case False have a4: "¬((current s ≠ TEE sc)∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS2))" using False by blast let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?client_type = "param4 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?t_rev_event = "?t⦇exec_prime := tl ?exec⦈" let ?s_rev_event2 = "Driver_Read ?s_rev_event smc_ex_init_read zx_mgr" let ?pre_param_ops = "TEE_pre_param_operation ?in_params" let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state ?s_rev_event))) (the ?ses_id)" let ?isSesIdinMgrSesIdList_t = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state ?t_rev_event))) (the ?ses_id)" let ?s_ret = "tee_ta_close_session_teeDomain2_preR sc ?s_rev_event2 ?ses_id ?client_type ?in_params ?out_params" let ?t_ret = "tee_ta_close_session_teeDomain2_pre sc ?t_rev_event ?ses_id ?client_type ?in_params ?out_params" let ?exec_t = "(exec_prime ?t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?client_type_t = "param4 ?p_t" let ?cmd_id_t = "param6 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?pre_param_ops_t = "TEE_pre_param_operation ?in_params_t" show ?thesis proof (cases "(?pre_param_ops ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList = False)") case True have a5: "(?pre_param_ops ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList = False)" using True by blast have a6: "?t_rev_event=⇑(?s_rev_event)" by auto have a7: "?t_rev_event=⇑(?s_rev_event2)" using Driver_Read_not_change_old by auto show ?thesis using a6 TEEC_CloseSession2_def a4 a5 by (smt (verit) State.fold_congs(6) State.simps(4) TEEC_CloseSession2R_def a0 abstract_state_def fst_conv) next case False have a8: "¬((?pre_param_ops ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList = False))" using False by simp have a12: "?t_rev_event = ⇑(?s_rev_event2)" using Driver_Read_not_change_old by simp have a13: "(?s_rev_event2⇓(fst(?t_ret))) = (fst(?s_ret))" using tee_ta_close_session_teeDomain2_preR_def a12 by (metis fst_conv) have a9: "?s' = fst(?s_ret)" using TEEC_CloseSession2R_def a4 a8 by (smt (verit, del_insts) State.fold_congs(6) prod.collapse prod.inject) have b1: "¬(current ?t ≠ TEE sc∨(exec_prime ?t) = []∨snd (hd (exec_prime ?t)) ≠ TEEC_CS2∨?pre_param_ops_t ≠ TEE_SUCCESS∨?isSesIdinMgrSesIdList_t = False)" using a4 a8 by simp have a10: "?t' = fst(?t_ret)" using TEEC_CloseSession2_def b1 a0 State.fold_congs(6) fst_conv by (smt (verit) State.unfold_congs(1)) have a11: "fst(?t_ret) = ⇑(fst(?s_ret))" using a13 abs_rev_lemma by metis show ?thesis using a9 a10 a11 by argo qed qed }qed } then show ?thesis by blast qed lemma TEEC_CloseSession3R_refine: "∀s. fst (TEEC_CloseSession3 sc (⇑s)) = ⇑(fst (TEEC_CloseSession3R sc s))" proof - { fix s let ?s'="fst(TEEC_CloseSession3R sc s)" let ?t = "⇑s" let ?t' = "fst(TEEC_CloseSession3 sc ?t)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?t_rev_event = "?t⦇exec_prime := tl ?exec⦈" let ?isSesIdInTaStateSesList = "isSessIdInTaStateSessList (⇑s) ?ses_id ?servTid" let ?nextFuncStepParam = "⦇param1 = ?ses_id, param2 = ?servTid, param3 = None, param4 = ?clientType, param5 = None, param6 =None, param7 = ?in_params, param8 = ?out_params, param9 = None, param10=None, param11=None, param12=None, param13=None⦈" let ?s_taCloseSessionEntry = "TA_CloseSessionEntryPointR ?s_rev_event (the ?servTid)" let ?t_taCloseSessionEntry = "TA_CloseSessionEntryPoint ?t_rev_event (the ?servTid)" let ?s_removeSess_inTaState = "?s_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑?s_taCloseSessionEntry) (the ?ses_id) (the ?in_params) (the ?out_params))" let ?t_removeSess_inTaState = "removeAllSessIdInTaStateSessList ?t_taCloseSessionEntry (the ?ses_id) (the ?in_params) (the ?out_params)" let ?taState = "(TAs_state s) (the ?servTid)" let ?taSesListInTaState = "(TA_sessions (the ?taState))" let ?ta_attr = "TA_attribute (the ?taState)" let ?isSingleInstance = "singleInstance ?ta_attr" let ?isKeepAlive = "keepAlive ?ta_attr" have a80: "?t_rev_event = ⇑?s_rev_event" by simp have a8: "?t_taCloseSessionEntry = ⇑?s_taCloseSessionEntry" using TA_CloseSessionEntryPointR_refine a80 by metis have a9: "?t_removeSess_inTaState = ⇑?s_removeSess_inTaState" using a8 by simp have a0:"current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t" by simp have a01:"?t' =⇑(?s')" proof (cases "(current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS3)") case True have a1_1: "(current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS3)" using True by auto have a1_2: "(current ?t ≠ (the ?servTid))∨((exec_prime ?t) = [])∨(snd (hd (exec_prime ?t)) ≠ TEEC_CS3)" using a0 a1_1 by auto have a1: "?t=?t'" using TEEC_CloseSession3_def a1_2 by (smt (verit, ccfv_threshold) a0 fstI) have a2: "?s'=s" using TEEC_CloseSession3R_def a1_1 by (smt (verit, ccfv_threshold) a0 fstI) show ?thesis using a1 a2 by simp next case False have a3: "¬((current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS3))" using False by auto show ?thesis proof (cases "?isSesIdInTaStateSesList = False") case True let ?s_sesIdNotInTaStateSesList = "?s_rev_event⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_rev_event)⦈" let ?t_sesIdNotInTaStateSesList = "?t_rev_event⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?t_rev_event)⦈" have a4: "?t_sesIdNotInTaStateSesList = ⇑(?s_sesIdNotInTaStateSesList)" by auto have a5: "?s' = ?s_sesIdNotInTaStateSesList" using TEEC_CloseSession3R_def a3 True by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have a6: "?t' = ?t_sesIdNotInTaStateSesList" using TEEC_CloseSession3_def a3 True a0 by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) show ?thesis using a4 a5 a6 TEEC_CloseSession3_def TEEC_CloseSession3R_def a3 True by metis next case False have a7: "¬(?isSesIdInTaStateSesList = False)" using False by simp show ?thesis proof (cases "¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = []") case True let ?s_taDestroyEntryPoint = "(?s_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑?s_removeSess_inTaState)))" let ?s_deleteTaStateBackTEE = "?s_taDestroyEntryPoint⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_taDestroyEntryPoint)⦈" let ?t_taDestroyEntryPoint = "TA_DestroyEntryPoint ?t_removeSess_inTaState" let ?t_deleteTaStateBackTEE = "?t_taDestroyEntryPoint⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?t_taDestroyEntryPoint)⦈" have a10: "?t_taDestroyEntryPoint = ⇑?s_taDestroyEntryPoint" using a9 by auto have a11: "?t_deleteTaStateBackTEE = ⇑?s_deleteTaStateBackTEE" using a10 by auto have a12: "?s' = ?s_deleteTaStateBackTEE" using TEEC_CloseSession3R_def True a3 a7 by (smt (verit) State.unfold_congs(1) State.unfold_congs(6) abs_rev_lemma fst_conv) have a13: "?t' = ?t_deleteTaStateBackTEE" using TEEC_CloseSession3_def True a3 a7 by (smt (verit) State.unfold_congs(1) State.unfold_congs(6) TA_DestroyEntryPoint_def a0 fst_conv) show ?thesis using a11 a12 a13 TEEC_CloseSession3_def TEEC_CloseSession3R_def True a3 a7 by metis next case False have a14: "¬(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])" using False by simp let ?s_notDeleteTaStateBackTEE = "?s_removeSess_inTaState⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_removeSess_inTaState)⦈" let ?t_notDeleteTaStateBackTEE = "?t_removeSess_inTaState⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?t_removeSess_inTaState)⦈" have a15: "?t_notDeleteTaStateBackTEE = ⇑(?s_notDeleteTaStateBackTEE)" using a9 by auto have a16: "?t' = ?t_notDeleteTaStateBackTEE" using TEEC_CloseSession3_def a3 a7 a14 by (smt (verit) State.unfold_congs(1) State.unfold_congs(6) TA_DestroyEntryPoint_def a0 fst_conv) have a17: "?s' = ?s_notDeleteTaStateBackTEE" using TEEC_CloseSession3R_def a3 a7 a14 by (smt (verit) State.unfold_congs(1) State.unfold_congs(6) abs_rev_lemma fst_conv) show ?thesis using a15 a16 a17 by simp qed qed qed } then show ?thesis by blast qed lemma TEEC_CloseSession4R_refine: "∀s. fst (TEEC_CloseSession4 sc (⇑s)) = ⇑(fst (TEEC_CloseSession4R sc s))" proof - { fix s let ?s'="fst(TEEC_CloseSession4R sc s)" let ?t = "⇑s" let ?t' = "fst(TEEC_CloseSession4 sc ?t)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?t_rev_event = "?t⦇exec_prime := tl ?exec⦈" let ?mgrSes = "the(findMgrSessionFromList (⇑s) (the ?ses_id))" let ?clientType = "client_id ?mgrSes" let ?loginType = "login ?clientType" let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))" let ?curMgrTaIns = "findTaInsInMgrByTid ?mgrTaInsList (the ?servTid)" let ?curMgrTaIns_attr = "attribute (the ?curMgrTaIns)" let ?isSingleInstance = "singleInstance ?curMgrTaIns_attr" let ?isKeepAlive = "keepAlive ?curMgrTaIns_attr" let ?curMgrTaIns_refCnt = "reference_cnt (the ?curMgrTaIns) - 1" let ?s_removeSess_inMgrTaSes = "?s_rev_event⇓(removeAllSessionInMgrSesList (⇑?s_rev_event) (the ?ses_id))" let ?t_removeSess_inMgrTaSes = "removeAllSessionInMgrSesList ?t_rev_event (the ?ses_id)" let ?s_setNotBusy = "?s_removeSess_inMgrTaSes⇓(setTaInsBusyByThreadId (⇑?s_removeSess_inMgrTaSes) (the ?servTid) False)" let ?t_setNotBusy = "setTaInsBusyByThreadId ?t_removeSess_inMgrTaSes (the ?servTid) False" let ?s_subRef = "?s_setNotBusy⇓(fst(subtractMgrInsRef (⇑?s_setNotBusy) (the ?servTid)))" let ?t_subRef = "(fst(subtractMgrInsRef ?t_setNotBusy (the ?servTid)))" let ?s_subRefR = "fst(Driver_Write_smc ?s_subRef zx_mgr ZX_OKr smc_ex_init)" have b1: "?t_rev_event = ⇑?s_rev_event" by simp have b2: "?t_removeSess_inMgrTaSes = ⇑?s_removeSess_inMgrTaSes" using b1 by simp have b3: "?t_setNotBusy = ⇑?s_setNotBusy" using b2 abs_rev_lemma by metis have b4: "?t_subRef = ⇑?s_subRef" using b3 abs_rev_lemma by metis have a0: "current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t" by simp have a01: "?t' =⇑(?s')" proof (cases "(current s ≠ (TEE sc))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS4)") case True have a02: "(current s ≠ (TEE sc))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS4)" using True by simp have a03: "(current ?t ≠ (TEE sc))∨((exec_prime ?t) = [])∨(snd (hd (exec_prime ?t)) ≠ TEEC_CS4)" using True by simp have a1: "?t'=?t" using TEEC_CloseSession4_def a03 by (smt (verit, ccfv_threshold) a0 fstI) have a2: "?s'=s" using TEEC_CloseSession4R_def a02 by (smt (verit, ccfv_threshold) a0 fstI) show ?thesis using a1 a2 by simp next case False have a3: "¬((current s ≠ (TEE sc))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS4))" using False by simp show ?thesis proof (cases "(?curMgrTaIns_refCnt = 0 ∧ (¬(?isKeepAlive = True ∧ ?isSingleInstance = True) | ?loginType = DTC_IDENTITY))") case True let ?curTa_curTaSessionList = "cur_ta_session_list (the ?curMgrTaIns)" let ?s_removeTaInTaIns = "?s_subRef⇓(fst(removeTaInsInMgrInsList (⇑?s_subRef) (the ?servTid)))" let ?t_removeTaInTaIns = "(fst(removeTaInsInMgrInsList ?t_subRef (the ?servTid)))" let ?s_closeCurTaInsSessList = "?s_removeTaInTaIns⇓((addCloseSessionEvent2 sc (⇑?s_removeTaInTaIns) (the ?in_params) (the ?out_params) ?curTa_curTaSessionList))" let ?t_closeCurTaInsSessList = "(addCloseSessionEvent2 sc ?t_removeTaInTaIns (the ?in_params) (the ?out_params) ?curTa_curTaSessionList)" let ?s_teeState_deleteCurTa = "?s_closeCurTaInsSessList⇓(deleteTaStateByThreadId (⇑?s_closeCurTaInsSessList) (the ?servTid))" let ?t_teeState_deleteCurTa = "deleteTaStateByThreadId ?t_closeCurTaInsSessList (the ?servTid)" let ?s_removeTaMemInTee = "?s_teeState_deleteCurTa⇓(removeTaMemInTeeDomain (⇑?s_teeState_deleteCurTa) (the ?servTid))" let ?t_removeTaMemInTee = "removeTaMemInTeeDomain ?t_teeState_deleteCurTa (the ?servTid)" let ?s_removeTaMemInTeeR = "fst(Driver_Write_smc ?s_removeTaMemInTee zx_mgr ZX_OKr smc_ex_init)" have a4: "?s' = ?s_removeTaMemInTeeR" using TEEC_CloseSession4R_def True a3 by (smt (verit) State.fold_congs(6) old.prod.inject prod.collapse) have a5: "?t' = ?t_removeTaMemInTee" using TEEC_CloseSession4_def True a3 by (smt (verit) State.fold_congs(6) a0 old.prod.inject prod.collapse) have a6: "?t_removeTaInTaIns = ⇑?s_removeTaInTaIns" using b4 abs_rev_lemma by metis have a7: "?t_closeCurTaInsSessList = ⇑?s_closeCurTaInsSessList" using a6 abs_rev_lemma by metis have a8: "?t_teeState_deleteCurTa = ⇑?s_teeState_deleteCurTa" using a7 abs_rev_lemma by metis have a9: "?t_removeTaMemInTee = ⇑?s_removeTaMemInTee" using a8 abs_rev_lemma by metis have a10: "?t_removeTaMemInTee = ⇑?s_removeTaMemInTeeR" using a8 abs_rev_lemma a4 a5 Driver_Write_smc_not_change_old by presburger show ?thesis using a4 a5 a9 a10 by metis next case False have a11: "¬(?curMgrTaIns_refCnt = 0 ∧ (¬(?isKeepAlive = True ∧ ?isSingleInstance = True) | ?loginType = DTC_IDENTITY))" using False by simp have a12: "?t' = ?t_subRef" using TEEC_CloseSession4_def a3 a11 by (smt (z3) State.fold_congs(6) a0 old.prod.inject prod.collapse) have a13: "?s' = ?s_subRefR" using TEEC_CloseSession4_def a3 a11 by (smt (verit) State.fold_congs(6) TEEC_CloseSession4R_def old.prod.inject prod.collapse) have a14: "?t_subRef = ⇑?s_subRefR" using b4 Driver_Write_smc_not_change_old by metis show ?thesis using a12 a13 a14 by metis qed qed } then show ?thesis by simp qed subsection "integrity" lemma TEEC_CloseSession1R_integrity: assumes p1: "a = hyperc' (TEEC_CLOSESESSION1 fd ses_id in_params out_params)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s' s d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" have b1:"s'=fst(TEEC_CloseSession1R sysconf s fd ses_id in_params out_params)" using exec_eventR_def a3 p1 by simp have b2:"(s ∼. d .∼Δ s')" using TEEC_CloseSession1R_notchnew b1 by blast } then show ?thesis by blast qed lemma TEEC_CloseSession1R_integrity_e: "integrity_new_e (hyperc' (TEEC_CLOSESESSION1 fd ses_id in_params out_params))" using TEEC_CloseSession1R_integrity integrity_new_e_def by metis lemma TEEC_CloseSession2R_integrity: assumes p1: "a = hyperc' (TEEC_CLOSESESSION2)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?client_type = "param4 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_rev_event2 = "Driver_Read ?s_rev_event smc_ex_init_read zx_mgr" let ?pre_param_ops = "TEE_pre_param_operation ?in_params" let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state ?s_rev_event))) (the ?ses_id)" let ?s_ret = "tee_ta_close_session_teeDomain2_preR sysconf ?s_rev_event2 ?ses_id ?client_type ?in_params ?out_params" have a4: "s'=fst(TEEC_CloseSession2R sysconf s)" using exec_eventR_def a3 p1 by simp have "(s ∼. d .∼Δ s')" proof (cases "(current s ≠ TEE sysconf)∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS2)") case True have "s' = s" using True a4 TEEC_CloseSession2R_def by (smt (verit, ccfv_threshold) fstI) then show ?thesis by simp next case False have a5: "¬((current s ≠ TEE sysconf)∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS2))" using False by simp show ?thesis proof (cases "(?pre_param_ops ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList = False)") case True have a6: "s' = ?s_rev_event" using True TEEC_CloseSession2R_def a4 a5 by (smt (z3) State.cases_scheme State.update_convs(6) prod.collapse prod.inject) show ?thesis using a6 by simp next case False have a8: "¬(?pre_param_ops ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList = False)" using False by simp have a9: "s' = fst(?s_ret)" using a4 a5 a8 TEEC_CloseSession2R_def by (smt (z3) False State.fold_congs(6) fstI) have "IPC_driver s = IPC_driver ?s_rev_event" by simp show ?thesis proof (cases "d=TEE sysconf") case True show ?thesis using True a2 interference1_def a5 domain_of_eventR_def by simp next case False have b1: "d≠TEE sysconf" using False by simp show ?thesis proof (cases "d = REE sysconf") case True then show ?thesis using True a2 interference1_def a5 domain_of_eventR_def by auto next case False have b2: "d ≠ REE sysconf" using False by simp have b3: "is_TA sysconf d" using b1 b2 by auto show ?thesis using b3 a2 interference1_def by simp qed qed qed qed } then show ?thesis by simp qed lemma TEEC_CloseSession2R_integrity_e: "integrity_new_e (hyperc' (TEEC_CLOSESESSION2))" using TEEC_CloseSession2R_integrity integrity_new_e_def by metis lemma TEEC_CloseSession3R_integrity: assumes p1: "a = hyperc' (TEEC_CLOSESESSION3)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" let ?domain = "the (domain_of_eventR s a)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?isSesIdInTaStateSesList = "isSessIdInTaStateSessList (⇑s) ?ses_id ?servTid" let ?nextFuncStepParam = "⦇param1 = ?ses_id, param2 = ?servTid, param3 = None, param4 = ?clientType, param5 = None, param6 =None, param7 = ?in_params, param8 = ?out_params, param9 = None, param10=None, param11=None, param12=None, param13=None⦈" let ?s_sesIdNotInTaStateSesList = "?s_rev_event⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_rev_event)⦈" let ?s_taCloseSessionEntry = "TA_CloseSessionEntryPointR ?s_rev_event (the ?servTid)" let ?s_removeSess_inTaState = "?s_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑?s_taCloseSessionEntry) (the ?ses_id) (the ?in_params) (the ?out_params))" let ?taState = "(TAs_state s) (the ?servTid)" let ?taSesListInTaState = "(TA_sessions (the ?taState))" let ?ta_attr = "TA_attribute (the ?taState)" let ?isSingleInstance = "singleInstance ?ta_attr" let ?isKeepAlive = "keepAlive ?ta_attr" have a4: "s'=fst(TEEC_CloseSession3R sysconf s)" using exec_eventR_def a3 p1 by simp have "(s ∼. d .∼Δ s')" proof (cases "(current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS3)") case True have "s= s'" using True TEEC_CloseSession3R_def a4 by (smt (verit, ccfv_threshold) fstI) then show ?thesis using vpeq_ipc_reflexive_lemma by blast next case False have b1: "¬((current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS3))" using False by auto show ?thesis proof (cases "?isSesIdInTaStateSesList = False") case True have a8:"s' = ?s_sesIdNotInTaStateSesList" using b1 True TEEC_CloseSession3R_def a4 by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have a9: "IPC_driver s = IPC_driver?s_rev_event" by simp have a10: "IPC_driver ?s_rev_event = IPC_driver ?s_sesIdNotInTaStateSesList" by simp have "IPC_driver s' = IPC_driver s" using a8 a9 a10 by simp then show ?thesis by simp next case False have b2: "¬(?isSesIdInTaStateSesList = False)" using False by simp show ?thesis proof (cases "(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])") case True let ?s_taDestroyEntryPoint = "(?s_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑?s_removeSess_inTaState)))" let ?s_deleteTaStateBackTEE = "?s_taDestroyEntryPoint⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_taDestroyEntryPoint)⦈" have a11: "s' = ?s_deleteTaStateBackTEE" using a4 TEEC_CloseSession3R_def True b1 b2 by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have a121: "IPC_driver ?s_deleteTaStateBackTEE = IPC_driver ?s_taDestroyEntryPoint" by simp have a122: "IPC_driver ?s_taDestroyEntryPoint = IPC_driver ?s_removeSess_inTaState" by simp have a123: "IPC_driver ?s_removeSess_inTaState = IPC_driver ?s_taCloseSessionEntry" by simp have a124: "IPC_driver ?s_taCloseSessionEntry = IPC_driver ?s_rev_event" using TA_CloseSessionEntryPointR_def by simp have a12: "IPC_driver s = IPC_driver ?s_deleteTaStateBackTEE" using a121 a122 a123 a124 by simp then show ?thesis using a11 vpeq_ipc_def by presburger next case False have b3: "¬(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])" using False by simp let ?s_notDeleteTaStateBackTEE = "?s_removeSess_inTaState⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_removeSess_inTaState)⦈" have a13: "s' = ?s_notDeleteTaStateBackTEE" using a4 b1 b2 b3 TEEC_CloseSession3R_def by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have a141: "IPC_driver ?s_notDeleteTaStateBackTEE = IPC_driver ?s_removeSess_inTaState" by simp have a142: "IPC_driver ?s_removeSess_inTaState = IPC_driver ?s_taCloseSessionEntry" by simp have a143: "IPC_driver ?s_taCloseSessionEntry = IPC_driver ?s_rev_event" using TA_CloseSessionEntryPointR_def by simp have a14: "IPC_driver s = IPC_driver ?s_notDeleteTaStateBackTEE" using a141 a142 a143 by simp then show ?thesis using a13 vpeq_ipc_def by presburger qed qed qed } then show ?thesis by simp qed lemma TEEC_CloseSession3R_integrity_e: "integrity_new_e (hyperc' (TEEC_CLOSESESSION3))" using TEEC_CloseSession3R_integrity integrity_new_e_def by metis lemma TEEC_CloseSession4R_integrity: assumes p1: "a = hyperc' (TEEC_CLOSESESSION4)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?mgrSes = "the(findMgrSessionFromList (⇑s) (the ?ses_id))" let ?clientType = "client_id ?mgrSes" let ?loginType = "login ?clientType" let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))" let ?curMgrTaIns = "findTaInsInMgrByTid ?mgrTaInsList (the ?servTid)" let ?curMgrTaIns_attr = "attribute (the ?curMgrTaIns)" let ?isSingleInstance = "singleInstance ?curMgrTaIns_attr" let ?isKeepAlive = "keepAlive ?curMgrTaIns_attr" let ?curMgrTaIns_refCnt = "reference_cnt (the ?curMgrTaIns) - 1" let ?s_removeSess_inMgrTaSes = "?s_rev_event⇓(removeAllSessionInMgrSesList (⇑?s_rev_event) (the ?ses_id))" let ?s_setNotBusy = "?s_removeSess_inMgrTaSes⇓(setTaInsBusyByThreadId (⇑?s_removeSess_inMgrTaSes) (the ?servTid) False)" let ?s_subRef = "?s_setNotBusy⇓(fst(subtractMgrInsRef (⇑?s_setNotBusy) (the ?servTid)))" let ?s_subRefR = "fst(Driver_Write_smc ?s_subRef zx_mgr ZX_OKr smc_ex_init)" have a4: "s'=fst(TEEC_CloseSession4R sysconf s)" using exec_eventR_def a3 p1 by simp have "(s ∼. d .∼Δ s')" proof (cases "(current s ≠ (TEE sysconf))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS4)") case True have "s' = s" using True TEEC_CloseSession4R_def a4 by (smt (verit, ccfv_threshold) fstI) then show ?thesis by simp next case False have b1: "¬((current s ≠ (TEE sysconf))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS4))" using False by simp show ?thesis proof (cases "(?curMgrTaIns_refCnt = 0 ∧ (¬(?isKeepAlive = True ∧ ?isSingleInstance = True) | ?loginType = DTC_IDENTITY))") case True let ?curTa_curTaSessionList = "cur_ta_session_list (the ?curMgrTaIns)" let ?s_removeTaInTaIns = "?s_subRef⇓(fst(removeTaInsInMgrInsList (⇑?s_subRef) (the ?servTid)))" let ?s_closeCurTaInsSessList = "?s_removeTaInTaIns⇓((addCloseSessionEvent2 sysconf (⇑?s_removeTaInTaIns) (the ?in_params) (the ?out_params) ?curTa_curTaSessionList))" let ?s_teeState_deleteCurTa = "?s_closeCurTaInsSessList⇓(deleteTaStateByThreadId (⇑?s_closeCurTaInsSessList) (the ?servTid))" let ?s_removeTaMemInTee = "?s_teeState_deleteCurTa⇓(removeTaMemInTeeDomain (⇑?s_teeState_deleteCurTa) (the ?servTid))" let ?s_removeTaMemInTeeR = "fst(Driver_Write_smc ?s_removeTaMemInTee zx_mgr ZX_OKr smc_ex_init)" show ?thesis proof (cases "d = TEE sysconf") case True then show ?thesis using a2 interference1_def b1 domain_of_eventR_def by auto next case False have c1: "d ≠ TEE sysconf" using False by simp show ?thesis proof (cases "d = REE sysconf") case True then show ?thesis using True a2 interference1_def b1 domain_of_eventR_def c1 is_TEE_def vpeq_ipc_def by presburger next case False have c2: "d ≠ REE sysconf" using False by simp have c3: "is_TA sysconf d" using c1 c2 by auto show ?thesis using c3 a2 interference1_def by simp qed qed next case False have b2: "¬(?curMgrTaIns_refCnt = 0 ∧ (¬(?isKeepAlive = True ∧ ?isSingleInstance = True) | ?loginType = DTC_IDENTITY))" using False by simp show ?thesis proof (cases "d = TEE sysconf") case True then show ?thesis using True a2 interference1_def b1 b2 domain_of_eventR_def by simp next case False have c4: "d ≠ TEE sysconf" using False by simp show ?thesis proof (cases "d = REE sysconf") case True then show ?thesis using True a2 interference1_def b1 b2 domain_of_eventR_def c4 is_TEE_def vpeq_ipc_def by presburger next case False have c5: "d ≠ REE sysconf" using False by simp have c6: "is_TA sysconf d" using c4 c5 by auto show ?thesis using c6 a2 interference1_def by simp qed qed qed qed } then show ?thesis by simp qed lemma TEEC_CloseSession4R_integrity_e: "integrity_new_e (hyperc' (TEEC_CLOSESESSION4))" using TEEC_CloseSession4R_integrity integrity_new_e_def by metis subsection "weak" lemma TEEC_CloseSession1R_weak_confidentiality: assumes p1: "a = hyperc' (TEEC_CLOSESESSION1 fd ses_id in_params out_params)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof - { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" have b1:"s'=fst(TEEC_CloseSession1R sysconf s fd ses_id in_params out_params)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEEC_CloseSession1R sysconf t fd ses_id in_params out_params)" using exec_eventR_def a8 p1 by simp have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEEC_CloseSession1R_notchnew a3 vpeqR_def by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEEC_CloseSession1R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEEC_CLOSESESSION1 fd ses_id in_params out_params))" using TEEC_CloseSession1R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) lemma TEEC_CloseSession2R_weak_confidentiality: assumes p1: "a = hyperc' (TEEC_CLOSESESSION2)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof - { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a32:"ta_mgr(TEE_state s) =ta_mgr(TEE_state t)" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?client_type = "param4 ?p" let ?cmd_id = "param6 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?s_rev_event2 = "Driver_Read ?s_rev_event smc_ex_init_read zx_mgr" let ?pre_param_ops = "TEE_pre_param_operation ?in_params" let ?isSesIdinMgrSesIdList = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state ?s_rev_event))) (the ?ses_id)" let ?s_ret = "tee_ta_close_session_teeDomain2_preR sysconf ?s_rev_event2 ?ses_id ?client_type ?in_params ?out_params" let ?exec_t = "(exec_prime t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?client_type_t = "param4 ?p_t" let ?cmd_id_t = "param6 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?t_rev_event = "t⦇exec_prime := tl ?exec_t⦈" let ?t_rev_event2 = "Driver_Read ?t_rev_event smc_ex_init_read zx_mgr" let ?pre_param_ops_t = "TEE_pre_param_operation ?in_params_t" let ?isSesIdinMgrSesIdList_t = "isSesIdinMgrSesList (mgr_ta_sessions (ta_mgr (TEE_state ?t_rev_event))) (the ?ses_id_t)" let ?t_ret = "tee_ta_close_session_teeDomain2_preR sysconf ?t_rev_event2 ?ses_id_t ?client_type_t ?in_params_t ?out_params_t" have "s' ∼. d .∼Δ t'" proof - { have b1:"s'=fst(TEEC_CloseSession2R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEEC_CloseSession2R sysconf t)" using exec_eventR_def a8 p1 by simp have b3:"current s = current t" using domain_of_eventR_def a4 by simp have b31:"?ses_id = ?ses_id_t" using a31 by simp have b4:"?pre_param_ops = ?pre_param_ops_t" using a31 by simp have b5:"?isSesIdinMgrSesIdList = ?isSesIdinMgrSesIdList_t" using isSesIdinMgrSesList_cur_ta_session_listR a32 b31 by simp show ?thesis proof (cases "(current s ≠ TEE sysconf)∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS2)") case True have c1: "s' = s" using True b1 TEEC_CloseSession2R_def by (smt (verit, ccfv_threshold) fstI) have c2: "t' = t" using True b2 TEEC_CloseSession2R_def a31 b3 by (smt (verit, ccfv_threshold) fstI) then show ?thesis using a3 c1 c2 vpeq_ipc_def by simp next case False have d1: "¬((current s ≠ TEE sysconf)∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS2))" using False by simp have d11: "¬((current t ≠ TEE sysconf)∨((exec_prime t) = [])∨(snd (hd (exec_prime t)) ≠ TEEC_CS2))" using d1 a31 b3 by simp show ?thesis proof (cases "(?pre_param_ops ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList = False)") case True have d2: "(?pre_param_ops_t ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList_t = False)" using b4 b5 True by simp have c3: "s' = ?s_rev_event" using d1 True TEEC_CloseSession2R_def b1 by (smt (verit, ccfv_SIG) State.unfold_congs(6) fst_conv) have c4: "t' = ?t_rev_event" using d11 d2 TEEC_CloseSession2R_def b2 by (smt (verit, ccfv_SIG) State.unfold_congs(6) fst_conv) show ?thesis using c3 c4 a3 by simp next case False have d3: "¬((?pre_param_ops ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList = False))" using False by simp have d31: "¬((?pre_param_ops_t ≠ TEE_SUCCESS)∨(?isSesIdinMgrSesIdList_t = False))" using b4 b5 d3 by simp have c5: "s' = fst(?s_ret)" using b1 d1 d3 TEEC_CloseSession2R_def by (smt (z3) False State.fold_congs(6) fstI) have c6: "t' = fst(?t_ret)" using b2 d11 d31 TEEC_CloseSession2R_def by (smt (z3) False State.fold_congs(6) fstI) show ?thesis proof (cases "d = TEE sysconf") case True have c7:"vpeq_ipc ?s_rev_event d ?t_rev_event" using a3 by simp have c8:"vpeq_ipc ?s_rev_event2 d ?t_rev_event2" using c7 Driver_Read_def by simp have c9:"vpeq_ipc (fst(?s_ret)) d (fst(?t_ret))" using c8 tee_ta_close_session_teeDomain2_preR_notchnew by (smt (verit) vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) show ?thesis using c5 c6 c9 by blast next case False have d4: "d ≠ TEE sysconf" using False by simp show ?thesis proof (cases "d = REE sysconf") case True then show ?thesis using d4 is_TEE_def vpeq_ipc_def by presburger next case False then have c10: "is_TA sysconf d" using is_TA_def d4 by blast then have c11: "(s' ∼. d .∼Δ t') =True" by auto then show ?thesis by auto qed qed qed qed } qed } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEEC_CloseSession2R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEEC_CLOSESESSION2))" using TEEC_CloseSession2R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) lemma TEEC_CloseSession3R_weak_confidentiality: assumes p1: "a = hyperc' (TEEC_CLOSESESSION3)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof - { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a32:"TAs_state s = TAs_state t" assume a33:"ta_mgr(TEE_state s) =ta_mgr(TEE_state t)" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?isSesIdInTaStateSesList = "isSessIdInTaStateSessList (⇑s) ?ses_id ?servTid" let ?nextFuncStepParam = "⦇param1 = ?ses_id, param2 = ?servTid, param3 = None, param4 = ?clientType, param5 = None, param6 =None, param7 = ?in_params, param8 = ?out_params, param9 = None, param10=None, param11=None, param12=None, param13=None⦈" let ?s_taCloseSessionEntry = "TA_CloseSessionEntryPointR ?s_rev_event (the ?servTid)" let ?s_removeSess_inTaState = "?s_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑?s_taCloseSessionEntry) (the ?ses_id) (the ?in_params) (the ?out_params))" let ?taState = "(TAs_state s) (the ?servTid)" let ?taSesListInTaState = "(TA_sessions (the ?taState))" let ?ta_attr = "TA_attribute (the ?taState)" let ?isSingleInstance = "singleInstance ?ta_attr" let ?isKeepAlive = "keepAlive ?ta_attr" let ?exec_t = "(exec_prime t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?servTid_t = "(param2 ?p_t)" let ?clientType_t = "param4 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?t_rev_event = "t⦇exec_prime := tl ?exec_t⦈" let ?isSesIdInTaStateSesList_t = "isSessIdInTaStateSessList (⇑t) ?ses_id_t ?servTid_t" let ?nextFuncStepParam_t = "⦇param1 = ?ses_id_t, param2 = ?servTid_t, param3 = None, param4 = ?clientType_t, param5 = None, param6 =None, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10=None, param11=None, param12=None, param13=None⦈" let ?t_taCloseSessionEntry = "TA_CloseSessionEntryPointR ?t_rev_event (the ?servTid_t)" let ?t_removeSess_inTaState = "?t_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑?t_taCloseSessionEntry) (the ?ses_id_t) (the ?in_params_t) (the ?out_params_t))" let ?taState_t = "(TAs_state t) (the ?servTid_t)" let ?taSesListInTaState_t = "(TA_sessions (the ?taState_t))" let ?ta_attr_t = "TA_attribute (the ?taState_t)" let ?isSingleInstance_t = "singleInstance ?ta_attr_t" let ?isKeepAlive_t = "keepAlive ?ta_attr_t" have b1:"s'=fst(TEEC_CloseSession3R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEEC_CloseSession3R sysconf t)" using exec_eventR_def a8 p1 by simp have "s' ∼. d .∼Δ t'" proof - { have b3:"current s = current t" using a4 domain_of_eventR_def by auto have b31:"?servTid = ?servTid_t" using a31 by simp have b32:"?taState = ?taState_t" using b31 a32 by simp have b33:"?ta_attr = ?ta_attr_t" using b32 by simp have b34:"?isSingleInstance = ?isSingleInstance_t" using b33 by simp have b35:"?isKeepAlive = ?isKeepAlive_t" using b33 by simp have b36:"?ses_id = ?ses_id_t" using a31 by simp show ?thesis proof(cases "current s ≠ (the ?servTid) ∨ (exec_prime s) = [] ∨ snd (hd (exec_prime s)) ≠ TEEC_CS3") case True have d1: "current t ≠ (the ?servTid_t) ∨ (exec_prime t) = [] ∨ snd (hd (exec_prime t)) ≠ TEEC_CS3" using True b3 a31 by simp have c1: "s' = s" using b1 True TEEC_CloseSession3R_def by (smt (verit, ccfv_threshold) fstI) have c2: "t' = t" using b2 d1 TEEC_CloseSession3R_def by (smt (verit, ccfv_threshold) fstI) then show ?thesis using c1 c2 a3 by simp next case False have d2:"¬(current s ≠ (the ?servTid) ∨ (exec_prime s) = [] ∨ snd (hd (exec_prime s)) ≠ TEEC_CS3)" using False by simp have d21:"¬(current t ≠ (the ?servTid_t) ∨ (exec_prime t) = [] ∨ snd (hd (exec_prime t)) ≠ TEEC_CS3)" using d2 b3 a31 by simp let ?s_sesIdNotInTaStateSesList = "?s_rev_event⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_rev_event)⦈" let ?t_sesIdNotInTaStateSesList = "?t_rev_event⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam_t, TEEC_CS4)#(exec_prime ?t_rev_event)⦈" show ?thesis proof (cases "?isSesIdInTaStateSesList = False") case True have d3:"?isSesIdInTaStateSesList_t = False" using True isSessIdInTaStateSessList_def a31 a32 by simp have c3:"s' = ?s_sesIdNotInTaStateSesList" using b1 d2 True TEEC_CloseSession3R_def by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have c4:"t' = ?t_sesIdNotInTaStateSesList" using b2 d21 d3 TEEC_CloseSession3R_def by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have c5:"vpeq_ipc ?s_sesIdNotInTaStateSesList d ?t_sesIdNotInTaStateSesList" using a3 by simp show ?thesis using c3 c4 c5 by blast next case False have d3:"¬(?isSesIdInTaStateSesList = False)" using False by simp have d31:"¬(?isSesIdInTaStateSesList_t = False)" using d3 isSessIdInTaStateSessList_def a31 a32 by simp then show ?thesis proof (cases "(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])") case True let ?s_taDestroyEntryPoint = "(?s_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑?s_removeSess_inTaState)))" let ?t_taDestroyEntryPoint = "(?t_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑?t_removeSess_inTaState)))" let ?s_deleteTaStateBackTEE = "?s_taDestroyEntryPoint⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_taDestroyEntryPoint)⦈" let ?t_deleteTaStateBackTEE = "?t_taDestroyEntryPoint⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam_t, TEEC_CS4)#(exec_prime ?t_taDestroyEntryPoint)⦈" have d4:"(¬(?isSingleInstance_t = True ∧ ?isKeepAlive_t = True) ∧ ?taSesListInTaState_t = [])" using True b32 b34 b35 by simp have c6:"s' = ?s_deleteTaStateBackTEE" using b1 True d3 d2 TEEC_CloseSession3R_def by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have c7:"t' = ?t_deleteTaStateBackTEE" using b2 d4 d31 d21 TEEC_CloseSession3R_def by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) show ?thesis proof (cases "d = TEE sysconf") case True have c8:"vpeq_ipc ?s_rev_event d ?t_rev_event" using a3 by simp have c9:"vpeq_ipc ?s_taCloseSessionEntry d ?t_taCloseSessionEntry" using c8 TA_CloseSessionEntryPointR_def by auto show ?thesis using c6 c7 c9 by auto next case False have d5:"d ≠ TEE sysconf" using False by simp show ?thesis proof (cases "d = REE sysconf") case True then show ?thesis using d5 is_TEE_def vpeq_ipc_def by simp next case False have d6:"d ≠ REE sysconf" using False by simp show ?thesis proof (cases "is_TA sysconf d") case True then show ?thesis using is_TA_def by simp next case False then show ?thesis using d5 d6 is_TA_def by blast qed qed qed next case False let ?s_notDeleteTaStateBackTEE = "?s_removeSess_inTaState⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEEC_CS4)#(exec_prime ?s_removeSess_inTaState)⦈" let ?t_notDeleteTaStateBackTEE = "?t_removeSess_inTaState⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam_t, TEEC_CS4)#(exec_prime ?t_removeSess_inTaState)⦈" have d7:"¬(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])" using False by simp have d71:"¬(¬(?isSingleInstance_t = True ∧ ?isKeepAlive_t = True) ∧ ?taSesListInTaState_t = [])" using b32 b34 b35 d7 by simp have c10:"s' = ?s_notDeleteTaStateBackTEE" using d2 d3 d7 TEEC_CloseSession3R_def b1 by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have c11:"t' = ?t_notDeleteTaStateBackTEE" using d21 d31 d71 TEEC_CloseSession3R_def b2 by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have c12:"vpeq_ipc ?s_rev_event d ?t_rev_event" using a3 by simp have c13:"vpeq_ipc ?s_taCloseSessionEntry d ?t_taCloseSessionEntry" using c12 TA_CloseSessionEntryPointR_def by auto have c14:"vpeq_ipc ?s_removeSess_inTaState d ?t_removeSess_inTaState" using c13 by simp have c15:"vpeq_ipc ?s_notDeleteTaStateBackTEE d ?t_notDeleteTaStateBackTEE" using c14 by auto show ?thesis using c10 c11 c15 by blast qed qed qed } qed } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEEC_CloseSession3R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEEC_CLOSESESSION3))" using TEEC_CloseSession3R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) lemma TEEC_CloseSession4R_weak_confidentiality: assumes p1: "a = hyperc' (TEEC_CLOSESESSION4)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof - { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a32:"ta_mgr(TEE_state s) = ta_mgr(TEE_state t)" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?mgrSes = "the(findMgrSessionFromList (⇑s) (the ?ses_id))" let ?clientType = "client_id ?mgrSes" let ?loginType = "login ?clientType" let ?mgrTaInsList = "mgr_ta_instances (ta_mgr (TEE_state s))" let ?curMgrTaIns = "findTaInsInMgrByTid ?mgrTaInsList (the ?servTid)" let ?curMgrTaIns_attr = "attribute (the ?curMgrTaIns)" let ?isSingleInstance = "singleInstance ?curMgrTaIns_attr" let ?isKeepAlive = "keepAlive ?curMgrTaIns_attr" let ?curMgrTaIns_refCnt = "reference_cnt (the ?curMgrTaIns) - 1" let ?s_removeSess_inMgrTaSes = "?s_rev_event⇓(removeAllSessionInMgrSesList (⇑?s_rev_event) (the ?ses_id))" let ?s_setNotBusy = "?s_removeSess_inMgrTaSes⇓(setTaInsBusyByThreadId (⇑?s_removeSess_inMgrTaSes) (the ?servTid) False)" let ?s_subRef = "?s_setNotBusy⇓(fst(subtractMgrInsRef (⇑?s_setNotBusy) (the ?servTid)))" let ?s_subRefR = "fst(Driver_Write_smc ?s_subRef zx_mgr ZX_OKr smc_ex_init)" let ?exec_t = "(exec_prime t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?servTid_t = "(param2 ?p_t)" let ?clientType_t = "param4 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?t_rev_event = "t⦇exec_prime := tl ?exec_t⦈" let ?mgrSes_t = "the(findMgrSessionFromList (⇑t) (the ?ses_id_t))" let ?clientType_t = "client_id ?mgrSes_t" let ?loginType_t = "login ?clientType_t" let ?mgrTaInsList_t = "mgr_ta_instances (ta_mgr (TEE_state t))" let ?curMgrTaIns_t = "findTaInsInMgrByTid ?mgrTaInsList_t (the ?servTid_t)" let ?curMgrTaIns_attr_t = "attribute (the ?curMgrTaIns_t)" let ?isSingleInstance_t = "singleInstance ?curMgrTaIns_attr_t" let ?isKeepAlive_t = "keepAlive ?curMgrTaIns_attr_t" let ?curMgrTaIns_refCnt_t = "reference_cnt (the ?curMgrTaIns_t) - 1" let ?t_removeSess_inMgrTaSes = "?t_rev_event⇓(removeAllSessionInMgrSesList (⇑?t_rev_event) (the ?ses_id_t))" let ?t_setNotBusy = "?t_removeSess_inMgrTaSes⇓(setTaInsBusyByThreadId (⇑?t_removeSess_inMgrTaSes) (the ?servTid_t) False)" let ?t_subRef = "?t_setNotBusy⇓(fst(subtractMgrInsRef (⇑?t_setNotBusy) (the ?servTid_t)))" let ?t_subRefR = "fst(Driver_Write_smc ?t_subRef zx_mgr ZX_OKr smc_ex_init)" have b1:"s'=fst(TEEC_CloseSession4R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEEC_CloseSession4R sysconf t)" using exec_eventR_def a8 p1 by simp have b3:"current s = current t" using a4 domain_of_eventR_def by auto have b31:"?servTid = ?servTid_t" using a31 by simp have b32:"?mgrSes = ?mgrSes_t" using a31 a32 b31 findMgrSessionFromList_def by simp have b33:"?loginType = ?loginType_t" using b32 by simp have b34:"?mgrTaInsList = ?mgrTaInsList_t" using a32 by simp have b35:"?curMgrTaIns = ?curMgrTaIns_t" using b34 b31 findTaInsInMgrByTid_def by simp have b36:"?ses_id = ?ses_id_t" using a31 by simp have b37:"?curMgrTaIns_attr = ?curMgrTaIns_attr_t" using b35 by simp have b38:"?isSingleInstance = ?isSingleInstance_t" using b37 by simp have b39:"?isKeepAlive = ?isKeepAlive_t" using b37 by simp have b40:"?curMgrTaIns_refCnt = ?curMgrTaIns_refCnt_t" using b35 by simp have b41:"vpeq_ipc ?s_rev_event d ?t_rev_event" using a3 by simp have b42:"vpeq_ipc ?s_removeSess_inMgrTaSes d ?t_removeSess_inMgrTaSes" using b41 by auto have b43:"vpeq_ipc ?s_setNotBusy d ?t_setNotBusy" using a3 by simp have b44:"vpeq_ipc ?s_subRef d ?t_subRef" using b43 by auto have b45:"vpeq_ipc ?s_subRefR d ?t_subRefR" using b44 Driver_Write_smc_def by auto have "s' ∼. d .∼Δ t'" proof (cases "(current s ≠ (TEE sysconf))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS4)") case True have d1:"(current t ≠ (TEE sysconf))∨((exec_prime t) = [])∨(snd (hd (exec_prime t)) ≠ TEEC_CS4)" using b3 a31 True by simp have c1:"s = s'" using b1 True TEEC_CloseSession4R_def by (smt (verit, ccfv_threshold) fstI) have c2:"t' = t" using b2 d1 TEEC_CloseSession4R_def by (smt (verit, ccfv_threshold) fstI) show ?thesis using c1 c2 a3 vpeqR_def by blast next case False have d2:"¬((current s ≠ (TEE sysconf))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEEC_CS4))" using False by simp have d21:"¬((current t ≠ (TEE sysconf))∨((exec_prime t) = [])∨(snd (hd (exec_prime t)) ≠ TEEC_CS4))" using d2 b3 a31 by simp show ?thesis proof (cases "(?curMgrTaIns_refCnt = 0 ∧ (¬(?isKeepAlive = True ∧ ?isSingleInstance = True) | ?loginType = DTC_IDENTITY))") case True have d3:"(?curMgrTaIns_refCnt_t = 0 ∧ (¬(?isKeepAlive_t = True ∧ ?isSingleInstance_t = True) | ?loginType_t = DTC_IDENTITY))" using True b33 b40 b39 b37 by simp let ?curTa_curTaSessionList = "cur_ta_session_list (the ?curMgrTaIns)" let ?s_removeTaInTaIns = "?s_subRef⇓(fst(removeTaInsInMgrInsList (⇑?s_subRef) (the ?servTid)))" let ?s_closeCurTaInsSessList = "?s_removeTaInTaIns⇓((addCloseSessionEvent2 sysconf (⇑?s_removeTaInTaIns) (the ?in_params) (the ?out_params) ?curTa_curTaSessionList))" let ?s_teeState_deleteCurTa = "?s_closeCurTaInsSessList⇓(deleteTaStateByThreadId (⇑?s_closeCurTaInsSessList) (the ?servTid))" let ?s_removeTaMemInTee = "?s_teeState_deleteCurTa⇓(removeTaMemInTeeDomain (⇑?s_teeState_deleteCurTa) (the ?servTid))" let ?s_removeTaMemInTeeR = "fst(Driver_Write_smc ?s_removeTaMemInTee zx_mgr ZX_OKr smc_ex_init)" let ?curTa_curTaSessionList_t = "cur_ta_session_list (the ?curMgrTaIns_t)" let ?t_removeTaInTaIns = "?t_subRef⇓(fst(removeTaInsInMgrInsList (⇑?t_subRef) (the ?servTid_t)))" let ?t_closeCurTaInsSessList = "?t_removeTaInTaIns⇓((addCloseSessionEvent2 sysconf (⇑?t_removeTaInTaIns) (the ?in_params_t) (the ?out_params_t) ?curTa_curTaSessionList_t))" let ?t_teeState_deleteCurTa = "?t_closeCurTaInsSessList⇓(deleteTaStateByThreadId (⇑?t_closeCurTaInsSessList) (the ?servTid_t))" let ?t_removeTaMemInTee = "?t_teeState_deleteCurTa⇓(removeTaMemInTeeDomain (⇑?t_teeState_deleteCurTa) (the ?servTid_t))" let ?t_removeTaMemInTeeR = "fst(Driver_Write_smc ?t_removeTaMemInTee zx_mgr ZX_OKr smc_ex_init)" have c3:"s' = ?s_removeTaMemInTeeR" using d2 True TEEC_CloseSession4R_def b1 by (smt (z3) False State.fold_congs(6) old.prod.inject prod.collapse) have c4:"t' = ?t_removeTaMemInTeeR" using d21 d3 TEEC_CloseSession4R_def b2 by (smt (z3) False State.fold_congs(6) old.prod.inject prod.collapse) show ?thesis proof (cases "d = TEE sysconf") case True have c5:"vpeq_ipc ?s_removeTaInTaIns d ?t_removeTaInTaIns" using b44 by auto have c6:"vpeq_ipc ?s_closeCurTaInsSessList d ?t_closeCurTaInsSessList" using c5 by fastforce have c7:"vpeq_ipc ?s_teeState_deleteCurTa d ?t_teeState_deleteCurTa" using c6 by auto have c8:"vpeq_ipc ?s_removeTaMemInTee d ?t_removeTaMemInTee" using c7 by auto have c9:"vpeq_ipc ?s_removeTaMemInTeeR d ?t_removeTaMemInTeeR" using c8 Driver_Write_smc_def by auto show ?thesis using c3 c4 c9 by blast next case False have d3:"d ≠ TEE sysconf" using False by simp show ?thesis proof (cases "d = REE sysconf") case True then show ?thesis using d3 is_TEE_def vpeq_ipc_def by simp next case False have d4:"d ≠ REE sysconf" using False by simp show ?thesis proof (cases "is_TA sysconf d") case True then show ?thesis using is_TA_def by simp next case False then show ?thesis using d3 d4 is_TA_def by simp qed qed qed next case False have d5:"¬(?curMgrTaIns_refCnt = 0 ∧ (¬(?isKeepAlive = True ∧ ?isSingleInstance = True) | ?loginType = DTC_IDENTITY))" using False by simp have d51:"¬(?curMgrTaIns_refCnt_t = 0 ∧ (¬(?isKeepAlive_t = True ∧ ?isSingleInstance_t = True) | ?loginType_t = DTC_IDENTITY))" using d5 b40 b39 b38 b32 by simp have c10:"s' = ?s_subRefR" using d5 d2 TEEC_CloseSession4R_def b1 by (smt (z3) False State.fold_congs(6) old.prod.inject prod.collapse) have c11:"t' = ?t_subRefR" using d51 d21 TEEC_CloseSession4R_def b2 by (smt (z3) False State.fold_congs(6) old.prod.inject prod.collapse) show ?thesis using c10 c11 b45 by blast qed qed } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEEC_CloseSession4R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEEC_CLOSESESSION4))" using TEEC_CloseSession4R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) section "TEE side" subsection "refine" lemma TEE_CloseTASession1R_refine: "∀s. fst (TEE_CloseTASession1 sc (⇑s)) = ⇑(fst (TEE_CloseTASession1R sc s))" by (metis TEE_CloseTASession1R_def abs_rev_lemma fst_eqD) lemma TEE_CloseTASession2R_refine: "∀s. fst (TEE_CloseTASession2 sc (⇑s)) = ⇑(fst (TEE_CloseTASession2R sc s))" by (metis TEE_CloseTASession2R_def abs_rev_lemma fst_eqD) lemma TEE_CloseTASession3R_refine: "∀s. fst (TEE_CloseTASession3 sc (⇑s)) = ⇑(fst (TEE_CloseTASession3R sc s))" proof - { fix s let ?s'="fst(TEE_CloseTASession3R sc s)" let ?t = "⇑s" let ?t' = "fst(TEE_CloseTASession3 sc ?t)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?t_rev_event = "?t⦇exec_prime := tl ?exec⦈" let ?isSesIdInTaStateSesList = "isSessIdInTaStateSessList (⇑s) ?ses_id ?servTid" let ?nextFuncStepParam = "⦇param1 = ?ses_id, param2 = ?servTid, param3 = None, param4 = ?clientType, param5 = None, param6 =None, param7 = ?in_params, param8 = ?out_params, param9 = None, param10=None, param11=None, param12=None, param13=None⦈" let ?s_taCloseSessionEntry = "TA_CloseSessionEntryPointR ?s_rev_event (the ?servTid)" let ?t_taCloseSessionEntry = "TA_CloseSessionEntryPoint ?t_rev_event (the ?servTid)" let ?s_removeSess_inTaState = "?s_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑?s_taCloseSessionEntry) (the ?ses_id) (the ?in_params) (the ?out_params))" let ?t_removeSess_inTaState = "removeAllSessIdInTaStateSessList ?t_taCloseSessionEntry (the ?ses_id) (the ?in_params) (the ?out_params)" let ?taState = "(TAs_state s) (the ?servTid)" let ?taSesListInTaState = "(TA_sessions (the ?taState))" let ?ta_attr = "TA_attribute (the ?taState)" let ?isSingleInstance = "singleInstance ?ta_attr" let ?isKeepAlive = "keepAlive ?ta_attr" have a80: "?t_rev_event = ⇑?s_rev_event" by simp have a8: "?t_taCloseSessionEntry = ⇑?s_taCloseSessionEntry" using TA_CloseSessionEntryPointR_refine a80 by metis have a9: "?t_removeSess_inTaState = ⇑?s_removeSess_inTaState" using a8 by simp have a0:"current s=current ?t∧TEE_state s =TEE_state ?t∧exec_prime s=exec_prime ?t" by simp have a01:"?t' =⇑(?s')" proof (cases "(current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEE_CS3)") case True have a1_1: "(current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEE_CS3)" using True by auto have a1_2: "(current ?t ≠ (the ?servTid))∨((exec_prime ?t) = [])∨(snd (hd (exec_prime ?t)) ≠ TEE_CS3)" using a0 a1_1 by auto have a1: "?t=?t'" using TEE_CloseTASession3_def a1_2 by (smt (verit, ccfv_threshold) a0 fstI) have a2: "?s'=s" using TEE_CloseTASession3R_def a1_1 by (smt (verit, ccfv_threshold) a0 fstI) show ?thesis using a1 a2 by simp next case False have a3: "¬((current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEE_CS3))" using False by auto show ?thesis proof (cases "?isSesIdInTaStateSesList = False") case True let ?s_sesIdNotInTaStateSesList = "?s_rev_event⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_rev_event)⦈" let ?t_sesIdNotInTaStateSesList = "?t_rev_event⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?t_rev_event)⦈" have a4: "?t_sesIdNotInTaStateSesList = ⇑(?s_sesIdNotInTaStateSesList)" by auto have a5: "?s' = ?s_sesIdNotInTaStateSesList" using TEE_CloseTASession3R_def a3 True by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have a6: "?t' = ?t_sesIdNotInTaStateSesList" using TEE_CloseTASession3_def a3 True a0 by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) show ?thesis using a4 a5 a6 TEE_CloseTASession3_def TEE_CloseTASession3R_def a3 True by metis next case False have a7: "¬(?isSesIdInTaStateSesList = False)" using False by simp show ?thesis proof (cases "¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = []") case True let ?s_taDestroyEntryPoint = "(?s_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑?s_removeSess_inTaState)))" let ?s_deleteTaStateBackTEE = "?s_taDestroyEntryPoint⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_taDestroyEntryPoint)⦈" let ?t_taDestroyEntryPoint = "TA_DestroyEntryPoint ?t_removeSess_inTaState" let ?t_deleteTaStateBackTEE = "?t_taDestroyEntryPoint⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?t_taDestroyEntryPoint)⦈" have a10: "?t_taDestroyEntryPoint = ⇑?s_taDestroyEntryPoint" using a9 by auto have a11: "?t_deleteTaStateBackTEE = ⇑?s_deleteTaStateBackTEE" using a10 by auto have a12: "?s' = ?s_deleteTaStateBackTEE" using TEE_CloseTASession3R_def True a3 a7 by (smt (verit) State.unfold_congs(1) State.unfold_congs(6) abs_rev_lemma fst_conv) have a13: "?t' = ?t_deleteTaStateBackTEE" using TEE_CloseTASession3_def True a3 a7 by (smt (verit) State.unfold_congs(1) State.unfold_congs(6) TA_DestroyEntryPoint_def a0 fst_conv) show ?thesis using a11 a12 a13 TEE_CloseTASession3_def TEE_CloseTASession3R_def True a3 a7 by metis next case False have a14: "¬(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])" using False by simp let ?s_notDeleteTaStateBackTEE = "?s_removeSess_inTaState⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_removeSess_inTaState)⦈" let ?t_notDeleteTaStateBackTEE = "?t_removeSess_inTaState⦇current := TEE sc, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?t_removeSess_inTaState)⦈" have a15: "?t_notDeleteTaStateBackTEE = ⇑(?s_notDeleteTaStateBackTEE)" using a9 by auto have a16: "?t' = ?t_notDeleteTaStateBackTEE" using TEE_CloseTASession3_def a3 a7 a14 TA_DestroyEntryPoint_def a0 by (smt (verit) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have a17: "?s' = ?s_notDeleteTaStateBackTEE" using TEE_CloseTASession3R_def a3 a7 a14 by (smt (verit) State.unfold_congs(1) State.unfold_congs(6) abs_rev_lemma fst_conv) show ?thesis using a15 a16 a17 by simp qed qed qed } then show ?thesis by blast qed lemma TEE_CloseTASession4R_refine: "∀s. fst (TEE_CloseTASession4 sc (⇑s)) = ⇑(fst (TEE_CloseTASession4R sc s))" by (metis TEE_CloseTASession4R_def abs_rev_lemma fst_eqD) subsection "integrity" lemma TEE_CloseTASession1R_integrity: assumes p1: "a = hyperc' (TEE_CLOSETASESSION1)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s' s d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" have b1:"s'=fst (TEE_CloseTASession1R sysconf s)" using exec_eventR_def a3 p1 by simp have b2:"(s ∼. d .∼Δ s')" using TEE_CloseTASession1R_notchnew b1 by blast } then show ?thesis by blast qed lemma TEE_CloseTASession1R_integrity_e: "integrity_new_e (hyperc' (TEE_CLOSETASESSION1))" using TEE_CloseTASession1R_integrity integrity_new_e_def by metis lemma TEE_CloseTASession2R_integrity: assumes p1: "a = hyperc' (TEE_CLOSETASESSION2)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s' s d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" have b1:"s'=fst (TEE_CloseTASession2R sysconf s)" using exec_eventR_def a3 p1 by simp have b2:"(s ∼. d .∼Δ s')" using TEE_CloseTASession2R_notchnew b1 by blast } then show ?thesis by blast qed lemma TEE_CloseTASession2R_integrity_e: "integrity_new_e (hyperc' (TEE_CLOSETASESSION2))" using TEE_CloseTASession2R_integrity integrity_new_e_def by metis lemma TEE_CloseTASession3R_integrity: assumes p1: "a = hyperc' (TEE_CLOSETASESSION3)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s s' d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" let ?domain = "the (domain_of_eventR s a)" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?isSesIdInTaStateSesList = "isSessIdInTaStateSessList (⇑s) ?ses_id ?servTid" let ?nextFuncStepParam = "⦇param1 = ?ses_id, param2 = ?servTid, param3 = None, param4 = ?clientType, param5 = None, param6 =None, param7 = ?in_params, param8 = ?out_params, param9 = None, param10=None, param11=None, param12=None, param13=None⦈" let ?s_sesIdNotInTaStateSesList = "?s_rev_event⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_rev_event)⦈" let ?s_taCloseSessionEntry = "TA_CloseSessionEntryPointR ?s_rev_event (the ?servTid)" let ?s_removeSess_inTaState = "?s_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑?s_taCloseSessionEntry) (the ?ses_id) (the ?in_params) (the ?out_params))" let ?taState = "(TAs_state s) (the ?servTid)" let ?taSesListInTaState = "(TA_sessions (the ?taState))" let ?ta_attr = "TA_attribute (the ?taState)" let ?isSingleInstance = "singleInstance ?ta_attr" let ?isKeepAlive = "keepAlive ?ta_attr" have a4: "s'=fst(TEE_CloseTASession3R sysconf s)" using exec_eventR_def a3 p1 by simp have "(s ∼. d .∼Δ s')" proof (cases "(current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEE_CS3)") case True have "s= s'" using True TEE_CloseTASession3R_def a4 by (smt (verit, ccfv_threshold) fstI) then show ?thesis using vpeq_ipc_reflexive_lemma by blast next case False have b1: "¬((current s ≠ (the ?servTid))∨((exec_prime s) = [])∨(snd (hd (exec_prime s)) ≠ TEE_CS3))" using False by auto show ?thesis proof (cases "?isSesIdInTaStateSesList = False") case True have a8:"s' = ?s_sesIdNotInTaStateSesList" using b1 True TEE_CloseTASession3R_def a4 by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have a9: "IPC_driver s = IPC_driver?s_rev_event" by simp have a10: "IPC_driver ?s_rev_event = IPC_driver ?s_sesIdNotInTaStateSesList" by simp have "IPC_driver s' = IPC_driver s" using a8 a9 a10 by simp then show ?thesis by simp next case False have b2: "¬(?isSesIdInTaStateSesList = False)" using False by simp show ?thesis proof (cases "(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])") case True let ?s_taDestroyEntryPoint = "(?s_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑?s_removeSess_inTaState)))" let ?s_deleteTaStateBackTEE = "?s_taDestroyEntryPoint⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_taDestroyEntryPoint)⦈" have a11: "s' = ?s_deleteTaStateBackTEE" using a4 TEE_CloseTASession3R_def True b1 b2 by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have a121: "IPC_driver ?s_deleteTaStateBackTEE = IPC_driver ?s_taDestroyEntryPoint" by simp have a122: "IPC_driver ?s_taDestroyEntryPoint = IPC_driver ?s_removeSess_inTaState" by simp have a123: "IPC_driver ?s_removeSess_inTaState = IPC_driver ?s_taCloseSessionEntry" by simp have a124: "IPC_driver ?s_taCloseSessionEntry = IPC_driver ?s_rev_event" using TA_CloseSessionEntryPointR_def by simp have a12: "IPC_driver s = IPC_driver ?s_deleteTaStateBackTEE" using a121 a122 a123 a124 by simp then show ?thesis using a11 vpeq_ipc_def by presburger next case False have b3: "¬(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])" using False by simp let ?s_notDeleteTaStateBackTEE = "?s_removeSess_inTaState⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_removeSess_inTaState)⦈" have a13: "s' = ?s_notDeleteTaStateBackTEE" using a4 b1 b2 b3 TEE_CloseTASession3R_def by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have a141: "IPC_driver ?s_notDeleteTaStateBackTEE = IPC_driver ?s_removeSess_inTaState" by simp have a142: "IPC_driver ?s_removeSess_inTaState = IPC_driver ?s_taCloseSessionEntry" by simp have a143: "IPC_driver ?s_taCloseSessionEntry = IPC_driver ?s_rev_event" using TA_CloseSessionEntryPointR_def by simp have a14: "IPC_driver s = IPC_driver ?s_notDeleteTaStateBackTEE" using a141 a142 a143 by simp then show ?thesis using a13 vpeq_ipc_def by presburger qed qed qed } then show ?thesis by simp qed lemma TEE_CloseTASession3R_integrity_e: "integrity_new_e (hyperc' (TEE_CLOSETASESSION3))" using TEE_CloseTASession3R_integrity integrity_new_e_def by metis lemma TEE_CloseTASession4R_integrity: assumes p1: "a = hyperc' (TEE_CLOSETASESSION4)" shows "∀ d s s'. reachable0 s ∧ ((the (domain_of_eventR s a)) ∖↝ d) ∧ (s, s') ∈ exec_eventR a ⟶ (s ∼. d .∼Δ s')" proof - { fix s' s d assume a1: "reachable0 s" assume a2: "((the (domain_of_eventR s a)) ∖↝ d)" assume a3: "(s,s') ∈ exec_eventR a" have b1:"s'=fst (TEE_CloseTASession4R sysconf s)" using exec_eventR_def a3 p1 by simp have b2:"(s ∼. d .∼Δ s')" using TEE_CloseTASession4R_notchnew b1 by blast } then show ?thesis by blast qed lemma TEE_CloseTASession4R_integrity_e: "integrity_new_e (hyperc' (TEE_CLOSETASESSION4))" using TEE_CloseTASession4R_integrity integrity_new_e_def by metis subsection "weak" lemma TEE_CloseTASession1R_weak_confidentiality: assumes p1: "a = hyperc' (TEE_CLOSETASESSION1)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof - { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" have b1:"s'=fst (TEE_CloseTASession1R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEE_CloseTASession1R sysconf t)" using exec_eventR_def a8 p1 by simp have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_CloseTASession1R_notchnew a3 vpeqR_def by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEE_CloseTASession1R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEE_CLOSETASESSION1))" using TEE_CloseTASession1R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) lemma TEE_CloseTASession2R_weak_confidentiality: assumes p1: "a = hyperc' (TEE_CLOSETASESSION2)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof - { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" have b1:"s'=fst (TEE_CloseTASession2R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEE_CloseTASession2R sysconf t)" using exec_eventR_def a8 p1 by simp have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_CloseTASession2R_notchnew a3 vpeqR_def by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEE_CloseTASession2R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEE_CLOSETASESSION2))" using TEE_CloseTASession2R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) lemma TEE_CloseTASession3R_weak_confidentiality: assumes p1: "a = hyperc' (TEE_CLOSETASESSION3)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof - { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a32:"TAs_state s = TAs_state t" assume a33:"ta_mgr(TEE_state s) =ta_mgr(TEE_state t)" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" let ?exec = "(exec_prime s)" let ?p = "fst (hd ?exec)" let ?ses_id = "param1 ?p" let ?servTid = "(param2 ?p)" let ?clientType = "param4 ?p" let ?in_params = "param7 ?p" let ?out_params = "param8 ?p" let ?s_rev_event = "s⦇exec_prime := tl ?exec⦈" let ?isSesIdInTaStateSesList = "isSessIdInTaStateSessList (⇑s) ?ses_id ?servTid" let ?nextFuncStepParam = "⦇param1 = ?ses_id, param2 = ?servTid, param3 = None, param4 = ?clientType, param5 = None, param6 =None, param7 = ?in_params, param8 = ?out_params, param9 = None, param10=None, param11=None, param12=None, param13=None⦈" let ?s_taCloseSessionEntry = "TA_CloseSessionEntryPointR ?s_rev_event (the ?servTid)" let ?s_removeSess_inTaState = "?s_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑?s_taCloseSessionEntry) (the ?ses_id) (the ?in_params) (the ?out_params))" let ?taState = "(TAs_state s) (the ?servTid)" let ?taSesListInTaState = "(TA_sessions (the ?taState))" let ?ta_attr = "TA_attribute (the ?taState)" let ?isSingleInstance = "singleInstance ?ta_attr" let ?isKeepAlive = "keepAlive ?ta_attr" let ?exec_t = "(exec_prime t)" let ?p_t = "fst (hd ?exec_t)" let ?ses_id_t = "param1 ?p_t" let ?servTid_t = "(param2 ?p_t)" let ?clientType_t = "param4 ?p_t" let ?in_params_t = "param7 ?p_t" let ?out_params_t = "param8 ?p_t" let ?t_rev_event = "t⦇exec_prime := tl ?exec_t⦈" let ?isSesIdInTaStateSesList_t = "isSessIdInTaStateSessList (⇑t) ?ses_id_t ?servTid_t" let ?nextFuncStepParam_t = "⦇param1 = ?ses_id_t, param2 = ?servTid_t, param3 = None, param4 = ?clientType_t, param5 = None, param6 =None, param7 = ?in_params_t, param8 = ?out_params_t, param9 = None, param10=None, param11=None, param12=None, param13=None⦈" let ?t_taCloseSessionEntry = "TA_CloseSessionEntryPointR ?t_rev_event (the ?servTid_t)" let ?t_removeSess_inTaState = "?t_taCloseSessionEntry⇓(removeAllSessIdInTaStateSessList (⇑?t_taCloseSessionEntry) (the ?ses_id_t) (the ?in_params_t) (the ?out_params_t))" let ?taState_t = "(TAs_state t) (the ?servTid_t)" let ?taSesListInTaState_t = "(TA_sessions (the ?taState_t))" let ?ta_attr_t = "TA_attribute (the ?taState_t)" let ?isSingleInstance_t = "singleInstance ?ta_attr_t" let ?isKeepAlive_t = "keepAlive ?ta_attr_t" have b1:"s'=fst(TEE_CloseTASession3R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEE_CloseTASession3R sysconf t)" using exec_eventR_def a8 p1 by simp have "s' ∼. d .∼Δ t'" proof - { have b3:"current s = current t" using a4 domain_of_eventR_def by auto have b31:"?servTid = ?servTid_t" using a31 by simp have b32:"?taState = ?taState_t" using b31 a32 by simp have b33:"?ta_attr = ?ta_attr_t" using b32 by simp have b34:"?isSingleInstance = ?isSingleInstance_t" using b33 by simp have b35:"?isKeepAlive = ?isKeepAlive_t" using b33 by simp have b36:"?ses_id = ?ses_id_t" using a31 by simp show ?thesis proof(cases "current s ≠ (the ?servTid) ∨ (exec_prime s) = [] ∨ snd (hd (exec_prime s)) ≠ TEE_CS3") case True have d1: "current t ≠ (the ?servTid_t) ∨ (exec_prime t) = [] ∨ snd (hd (exec_prime t)) ≠ TEE_CS3" using True b3 a31 by simp have c1: "s' = s" using b1 True TEE_CloseTASession3R_def by (smt (verit, ccfv_threshold) fstI) have c2: "t' = t" using b2 d1 TEE_CloseTASession3R_def by (smt (verit, ccfv_threshold) fstI) then show ?thesis using c1 c2 a3 by simp next case False have d2:"¬(current s ≠ (the ?servTid) ∨ (exec_prime s) = [] ∨ snd (hd (exec_prime s)) ≠ TEE_CS3)" using False by simp have d21:"¬(current t ≠ (the ?servTid_t) ∨ (exec_prime t) = [] ∨ snd (hd (exec_prime t)) ≠ TEE_CS3)" using d2 b3 a31 by simp let ?s_sesIdNotInTaStateSesList = "?s_rev_event⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_rev_event)⦈" let ?t_sesIdNotInTaStateSesList = "?t_rev_event⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam_t, TEE_CS4)#(exec_prime ?t_rev_event)⦈" show ?thesis proof (cases "?isSesIdInTaStateSesList = False") case True have d3:"?isSesIdInTaStateSesList_t = False" using True isSessIdInTaStateSessList_def a31 a32 by simp have c3:"s' = ?s_sesIdNotInTaStateSesList" using b1 d2 True TEE_CloseTASession3R_def by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have c4:"t' = ?t_sesIdNotInTaStateSesList" using b2 d21 d3 TEE_CloseTASession3R_def by (smt (verit, best) State.unfold_congs(1) State.unfold_congs(6) fst_conv) have c5:"vpeq_ipc ?s_sesIdNotInTaStateSesList d ?t_sesIdNotInTaStateSesList" using a3 by simp show ?thesis using c3 c4 c5 by blast next case False have d3:"¬(?isSesIdInTaStateSesList = False)" using False by simp have d31:"¬(?isSesIdInTaStateSesList_t = False)" using d3 isSessIdInTaStateSessList_def a31 a32 by simp then show ?thesis proof (cases "(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])") case True let ?s_taDestroyEntryPoint = "(?s_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑?s_removeSess_inTaState)))" let ?t_taDestroyEntryPoint = "(?t_removeSess_inTaState⇓(TA_DestroyEntryPoint (⇑?t_removeSess_inTaState)))" let ?s_deleteTaStateBackTEE = "?s_taDestroyEntryPoint⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_taDestroyEntryPoint)⦈" let ?t_deleteTaStateBackTEE = "?t_taDestroyEntryPoint⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam_t, TEE_CS4)#(exec_prime ?t_taDestroyEntryPoint)⦈" have d4:"(¬(?isSingleInstance_t = True ∧ ?isKeepAlive_t = True) ∧ ?taSesListInTaState_t = [])" using True b32 b34 b35 by simp have c6:"s' = ?s_deleteTaStateBackTEE" using b1 True d3 d2 TEE_CloseTASession3R_def by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have c7:"t' = ?t_deleteTaStateBackTEE" using b2 d4 d31 d21 TEE_CloseTASession3R_def by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) show ?thesis proof (cases "d = TEE sysconf") case True have c8:"vpeq_ipc ?s_rev_event d ?t_rev_event" using a3 by simp have c9:"vpeq_ipc ?s_taCloseSessionEntry d ?t_taCloseSessionEntry" using c8 TA_CloseSessionEntryPointR_def by auto show ?thesis using c6 c7 c9 by auto next case False have d5:"d ≠ TEE sysconf" using False by simp show ?thesis proof (cases "d = REE sysconf") case True then show ?thesis using d5 is_TEE_def vpeq_ipc_def by simp next case False have d6:"d ≠ REE sysconf" using False by simp show ?thesis proof (cases "is_TA sysconf d") case True then show ?thesis using is_TA_def by simp next case False then show ?thesis using d5 d6 is_TA_def by blast qed qed qed next case False let ?s_notDeleteTaStateBackTEE = "?s_removeSess_inTaState⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam, TEE_CS4)#(exec_prime ?s_removeSess_inTaState)⦈" let ?t_notDeleteTaStateBackTEE = "?t_removeSess_inTaState⦇current := TEE sysconf, exec_prime := (?nextFuncStepParam_t, TEE_CS4)#(exec_prime ?t_removeSess_inTaState)⦈" have d7:"¬(¬(?isSingleInstance = True ∧ ?isKeepAlive = True) ∧ ?taSesListInTaState = [])" using False by simp have d71:"¬(¬(?isSingleInstance_t = True ∧ ?isKeepAlive_t = True) ∧ ?taSesListInTaState_t = [])" using b32 b34 b35 d7 by simp have c10:"s' = ?s_notDeleteTaStateBackTEE" using d2 d3 d7 TEE_CloseTASession3R_def b1 by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have c11:"t' = ?t_notDeleteTaStateBackTEE" using d21 d31 d71 TEE_CloseTASession3R_def b2 by (smt (verit) State.fold_congs(1) State.fold_congs(6) fst_eqD) have c12:"vpeq_ipc ?s_rev_event d ?t_rev_event" using a3 by simp have c13:"vpeq_ipc ?s_taCloseSessionEntry d ?t_taCloseSessionEntry" using c12 TA_CloseSessionEntryPointR_def by auto have c14:"vpeq_ipc ?s_removeSess_inTaState d ?t_removeSess_inTaState" using c13 by simp have c15:"vpeq_ipc ?s_notDeleteTaStateBackTEE d ?t_notDeleteTaStateBackTEE" using c14 by auto show ?thesis using c10 c11 c15 by blast qed qed qed } qed } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEE_CloseTASession3R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEE_CLOSETASESSION3))" using TEE_CloseTASession3R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) lemma TEE_CloseTASession4R_weak_confidentiality: assumes p1: "a = hyperc' (TEE_CLOSETASESSION4)" shows "∀ d s t. reachable0 s ∧ reachable0 t ∧ (s ∼. d .∼ t) ∧ ((domain_of_eventR s a) = (domain_of_eventR t a)) ∧ (get_exec_primeR s=get_exec_primeR t) ∧ ((the (domain_of_eventR s a)) ↝ d) ∧ (s ∼. (the (domain_of_eventR s a)) .∼ t) ⟶ (∀ s' t'. (s, s') ∈ exec_eventR a ∧ (t, t') ∈ exec_eventR a ⟶ (s' ∼. d .∼Δ t'))" proof - { fix s t d s' t' assume a1:"reachable0 s" assume a2:"reachable0 t" assume a3:"s∼.d.∼t" assume a31:"exec_prime s=exec_prime t" assume a4:"(domain_of_eventR s a) = (domain_of_eventR t a)" assume a5:"(the (domain_of_eventR s a)) ↝ d" assume a6:"s ∼. (the (domain_of_eventR s a)) .∼ t" assume a7:"(s, s') ∈ exec_eventR a" assume a8:"(t, t') ∈ exec_eventR a" have b1:"s'=fst (TEE_CloseTASession4R sysconf s)" using exec_eventR_def a7 p1 by simp have b2:"t'=fst (TEE_CloseTASession4R sysconf t)" using exec_eventR_def a8 p1 by simp have b3:"s' ∼. d .∼Δ t'" using b1 b2 TEE_CloseTASession4R_notchnew a3 vpeqR_def by (meson vpeq_ipc_symmetric_lemma vpeq_ipc_transitive_lemma) } then show ?thesis using get_exec_primeR_def by (smt (verit, best) prod.inject) qed lemma TEE_CloseTASession4R_weak_confidentiality_e: "weak_confidentiality_new_e (hyperc' (TEE_CLOSETASESSION4))" using TEE_CloseTASession4R_weak_confidentiality weak_confidentiality_new_e_def get_exec_primeR_def by (smt (verit) Pair_inject) end